Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack: A Pledge for Formal Methods in the Field of Implementation Security

摘要

In our paper at PROOFS 2013, we formally studied a few known countermeasuresto protect CRT-RSA against the BellCoRe fault injection attack. However, weleft Vigilant's countermeasure and its alleged repaired version by Coron et al.as future work, because the arithmetical framework of our tool was notsufficiently powerful. In this paper we bridge this gap and then use the samemethodology to formally study both versions of the countermeasure. We obtainsurprising results, which we believe demonstrate the importance of formalanalysis in the field of implementation security. Indeed, the original versionof Vigilant's countermeasure is actually broken, but not as much as Coron etal. thought it was. As a consequence, the repaired version they proposed can besimplified. It can actually be simplified even further as two of the ninemodular verifications happen to be unnecessary. Fortunately, we could formallyprove the simplified repaired version to be resistant to the BellCoRe attack,which was considered a "challenging issue" by the authors of the countermeasurethemselves.